Inference at * 1 2 2 1 
Iof proof for Lemma sub-equality:

.....assertion..... NILNIL

1. T : Type
2. P : T
3. i : T
4. u : T
5. i = u
6. P(u)
7. P(i)
  u  {j:T| P(j)}  

latex

 by ((MemCD) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

{x:A| B(x)} , x:AB(x), s = t, f(a), t  T, , Type